constant\_function($f$; $A$; $B$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a$:$A$, ${\it a'}$:$A$. $f$($a$) = $f$(${\it a'}$) $\in$ $B$